\begin{tabbing}
fpf{-}sub($A$; $a$.$B$($a$); ${\it eq}$; $f$; $g$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\forall$$x$:$A$.\+
\\[0ex]fpf{-}dom(${\it eq}$; $x$; $f$) $\Rightarrow$ fpf{-}dom(${\it eq}$; $x$; $g$) \& fpf{-}ap($f$; ${\it eq}$; $x$) $=$ fpf{-}ap($g$; ${\it eq}$; $x$) $\in$ $B$($x$)
\-
\end{tabbing}